Specification zbranch-array-sorted

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

enrich
   zbranch-array
, 
   key-order
with
   

   
   
   
   predicates  sorted : zbranch-array × nat × nat;
               . ≤ . : key × key;
   
   
   
   

   

   axioms le-key :  ⊦ key0 ≤ key1 ↔ ¬ key1 < key0;
          used for: s, ls;
          sorted-base :  ⊦ sorted(zbrar, n, 0);
          used for: s, ls;
          sorted-one :  ⊦ sorted(zbrar, n, 1);
          used for: s, ls;
          sorted-rec :  ⊦ sorted(zbrar, n, m + 2) ↔ n < # zbrar ∧ zbrar[n].key < zbrar[n + 1].key ∧ sorted(zbrar, n + 1, m + 1);
          used for: s, ls;

   

   
end enrich